\begin{tabbing}
$\forall$\=$E$,$X_{1}$,$X_{2}$:Type, ${\it info}$:($E$$\rightarrow$((:Id $\times$ $X_{1}$) + (:(:IdLnk $\times$ $E$) $\times$ $X_{2}$))), ${\it pred?}$:($E$$\rightarrow$(?$E$)),\+
\\[0ex]$p$:(\=$\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$. 
\\[0ex]($\uparrow$rcv?(${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (link(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (((${\it e''}$ = ${\it e'}$) $\vee$ ${\it e''}$ $<$ ${\it e'}$) $\wedge$ (loc(${\it e'}$) = destination($l$) $\in$ Id)))),
\-\-\\[0ex]$e$:$E$, $l$:IdLnk. sends{-}bound($p$; $e$; $l$) $\in$ $E$
\-
\end{tabbing}